(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun n () Real)
(declare-fun k () Real)
(declare-fun d () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun l () Real)
(declare-fun g () Real)
(declare-fun m () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(assert (not (exists ((j Real)) (=> (and (=> (<= 0 j f) (<= j g)) (>= f 0) (= (/ c d) m) (> (/ a n) (+ m (/ (* l l) (* 2 (- (- b (- 680.2932226634903)) k))) (* (+ (/ p e) 1) (+ (* (/ p 2) g g) (* g l))))) (>= l 0) (<= l (/ 0 0)) (< (/ a n) i) (> (- (- b (- 680.2932226634903)) k) 0) (>= p 0)) (or (= h 7) (< o f) (> (/ a n) (+ (* f l) (/ (* l l) (* 2 (- (- b (- 680.2932226634903)) k))))))))))
(assert (= a (* n o)))
(assert (= o (/ a n)))
(assert (= b (+ e k (- 680.2932226634903))))
(assert (= d (/ c o)))
(assert (= o (/ c d)))
(check-sat)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun n () Real)
(declare-fun k () Real)
(declare-fun d () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun l () Real)
(declare-fun g () Real)
(declare-fun m () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(assert (not (exists ((j Real)) (=> (and (=> (<= 0 j f) (<= j g)) (>= f 0) (= (/ c d) m) (> (/ a n) (+ m (/ (* l l) (* 2 (- (- b (- 680.2932226634903)) k))) (* (+ (/ p e) 1) (+ (* (/ p 2) g g) (* g l))))) (>= l 0) (<= l (/ 0 0)) (< (/ a n) i) (> (- (- b (- 680.2932226634903)) k) 0) (>= p 0)) (or (= h 7) (< o f) (> (/ a n) (+ (* f l) (/ (* l l) (* 2 (- (- b (- 680.2932226634903)) k))))))))))
(assert (= a (* n o)))
(assert (= o (/ a n)))
(assert (= b (+ e k (- 680.2932226634903))))
(assert (= d (/ c o)))
(assert (= o (/ c d)))
(check-sat)
